home *** CD-ROM | disk | FTP | other *** search
/ Sprite 1984 - 1993 / Sprite 1984 - 1993.iso / lib / tex / inputs / vdm.sty < prev    next >
Encoding:
Text File  |  1991-05-21  |  37.1 KB  |  1,213 lines
  1. %
  2. %    VDM documentstyle option for LaTeX
  3. %
  4. %    M. Wolczko 
  5. %
  6. %    Created from the ashes of VDM.tex and CBJ's vdm86.tex
  7. %
  8. %    Uses the AMS msym fonts if available: if you don't have them,
  9. %    follow the instructions near the string FONT-CUSTOMIZING.
  10. %
  11. %    $Log:    vdm.doc,v $
  12. %    Revision 2.5  88/03/25  18:52:29  mario
  13. %    Improved use of AMS fonts.
  14. %    Improved efficiency by eliminating unnecessary macros.
  15. %    Enable line breaks after underscores in math mode.
  16. %    Fixed used of penalties....were in wrong placeto have any effect.
  17. %    Added \uniqueval, \cons, formbox environment, \R
  18. %    Fixed composite environments so that they can be used in horizontal
  19. %    mode.
  20. %    Fixed a bug in the proof environment.
  21. %
  22. %    Revision 2.4  87/11/12  12:31:07  mario
  23. %    Shortened lines for network mailers,
  24. %    Changed mathcodes of digits,
  25. %    Added \Rat, changed \DEF, added betweenFunctionAndPre hook,skip,
  26. %    and penalty, added \Conc
  27. %
  28. %    Revision 2.3  87/02/26  11:36:07  miw
  29. %    Absence of a blank line after \end{vdm} now forces \noindent.
  30. %    Can now have pre- and post-conditions in function defns.
  31. %    Added \mapinto macro.
  32. %
  33. %    Revision 2.2  86/12/18  12:00:17  miw
  34. %    Added \@changeMathmodeCatcodes to \begin{vdm} to avoid as many
  35. %    catcode problems with @ and _ as possible.
  36. %    Fixed a bug in \If (was adding extra blank lines).
  37. %    Added the \nexists macro.
  38. %    Added the *-form of fn (which had been inadvertently omitted).
  39. %    Fixed a bug in the proof environment (had a name clash with latex).
  40. %    
  41. %    Revision 2.1  86/11/24  13:08:34  miw
  42. %    **** MAJOR REWRITE/EXTENSION ****
  43. %    
  44. %    Entry to the vdm env now is a no-op!
  45. %    No mathcode changes to get the right letters in math mode.
  46. %    Double quotes now delimit text in math mode.
  47. %    \baselineskip within vdm mode is now \VDMbaselineskip.
  48. %    Added the \amssy font.
  49. %    Vertical VDM things (ops, fns, etc) shouldn't need blank lines
  50. %    around them. 
  51. %    Let the user choose whether some things are left- or right-aligned.
  52. %    Added *-forms of quantifiers.
  53. %    Added composite env and \scompose.
  54. %    Added proof env.
  55. %    
  56. %    Revision 1.8  86/10/08  14:11:36  miw
  57. %    Changed \or, \rd, \wr to \Or, \Rd, \Wr.
  58. %    Changed keyword font to sans-serif.
  59. %    Changed \makeNewKeyword to use \newcommand.
  60. %    Added \where keyword.
  61. %    Changed \Nat, \Int, \Bool, \Real to use `blackboard' font.
  62. %    Added `Strachey brackets' using \term.
  63. %    Added function composition, \compf.
  64. %    Added a *-form to the fn environment to omit parens on args.
  65. %    Added a *-form to \LambdaFn to place body on a new line.
  66. %    Added \min and \max monadic operators.
  67. %    Changed \serd and \busd to \rres and \rsub.
  68. %    Added \const for constants.
  69. %
  70. %    Revision 1.7  86/08/14  17:52:32  miw
  71. %    Fixed bugs in vdmfn and vdmop.
  72. %    Moved the pre..Hooks in operations and functions to occur earlier
  73. %    (allows one to change baselineskip).
  74. %
  75. %    Revision 1.6  86/06/03  12:23:05  miw
  76. %    Added the formula env, and fixed a bug in \type.
  77. %    
  78. %    
  79. %    Revision 1.5  86/05/07  17:51:48  miw
  80. %    Parameterised more vertical skips.  Changed many dimensions from pts
  81. %    to exs.  Fixed a bug in \type.  Altered externals so that field names
  82. %    are flush right.
  83. %    
  84. %    Revision 1.4  86/04/17  11:09:04  miw
  85. %    Tweaked some more.
  86. %
  87. %    Revision 1.3 86/03/14 20:44:22 miw
  88. %    Added left margin control with \VDMindent.
  89. %    Tweaked some penalties (esp. \hyphenpenalty)---first use of a
  90. %    \discretionary in quantified expresssion.
  91. %    Fixed a bug in IndentedPara (using box0 instead of copy0)
  92. %    
  93. %    Revision 1.2  86/03/12  16:26:23  miw
  94. %    Changed the fn env. and \Cases.  Added \@raggedRight.
  95. %    Fixed lots of other minor things.
  96. %
  97. %    Revision 1.1  86/03/03  18:42:40  miw
  98. %    Initial revision
  99. %
  100. %
  101. %    $Header: vdm.doc,v 2.5 88/03/25 18:52:29 mario Locked $
  102. %
  103. %
  104. %
  105. %----------------------------------------------------------------
  106. %
  107. %    Installation-dependent features
  108. %
  109. % FONT-CUSTOMIZING
  110. \newif\ifams@
  111. \ams@true  % change to \ams@false if you don't have the AMS fonts
  112. %\ams@false  % change to \ams@true if you have the AMS fonts
  113.  
  114. \newif\ifps@ \ps@false % PostScript-based
  115.  
  116. \def\@fmtname{lplain}
  117. \def\@psfmtname{pslplain}
  118.  
  119. \def\@testcmsy{\if@usecmsy \else 
  120.   \@latexerr{Can't use vdm with this PSLaTeX}%
  121.     {This PSLaTeX does not have the CMSY symbols
  122.     available, and cannot be used with VDM style.  Get
  123.     a guru to rebuild PSLaTeX with the CMSY and CMMI
  124.     fonts included.}\fi}
  125. \def\@testcmmi{\if@usecmmi \else
  126.   \@latexerr{Can't use vdm with this PSLaTeX}%
  127.     {This PSLaTeX does not have the CMMI symbols
  128.     available, and cannot be used with VDM style.  Get
  129.     a guru to rebuild PSLaTeX with the CMSY and CMMI
  130.     fonts included.}\fi}
  131.  
  132. \ifx\fmtname\@fmtname % standard LaTeX is OK
  133. \else \ifx\fmtname\@psfmtname \global\ps@true \@testcmsy \@testcmmi
  134.       \else \ams@false \fi\fi % don't use AMS for SliTeX
  135.  
  136. \newfam\msxfam
  137. \newfam\msyfam
  138.  
  139. \ifams@
  140.     % this is lifted from amssymbols.sty
  141.     \ifcase\@ptsize
  142.      \font\tenmsx=msxm10
  143.      \font\sevenmsx=msxm7
  144.      \font\fivemsx=msxm5
  145.      \font\tenmsy=msym10
  146.      \font\sevenmsy=msym7
  147.      \font\fivemsy=msym5
  148.     \or
  149.      \font\tenmsx=msxm10 scaled \magstephalf
  150.      \font\sevenmsx=msxm8
  151.      \font\fivemsx=msxm6
  152.      \font\tenmsy=msym10 scaled \magstephalf
  153.      \font\sevenmsy=msym8
  154.      \font\fivemsy=msym6
  155.     \or
  156.      \font\tenmsx=msxm10 scaled \magstep1
  157.      \font\sevenmsx=msxm8
  158.      \font\fivemsx=msxm6
  159.      \font\tenmsy=msym10 scaled \magstep1
  160.      \font\sevenmsy=msym8
  161.      \font\fivemsy=msym6
  162.     \fi
  163.  
  164.     \textfont\msxfam=\tenmsx  \scriptfont\msxfam=\sevenmsx
  165.       \scriptscriptfont\msxfam=\fivemsx
  166.     \textfont\msyfam=\tenmsy  \scriptfont\msyfam=\sevenmsy
  167.       \scriptscriptfont\msyfam=\fivemsy
  168.  
  169.     \def\hexnumber@#1{\ifnum#1<10 \number#1\else
  170.      \ifnum#1=10 A\else\ifnum#1=11 B\else\ifnum#1=12 C\else
  171.      \ifnum#1=13 D\else\ifnum#1=14 E\else
  172.      \ifnum#1=15 F\fi\fi\fi\fi\fi\fi\fi}
  173.     \def\msx@{\hexnumber@\msxfam}
  174.     \def\msy@{\hexnumber@\msyfam}
  175. \fi
  176.  
  177. %----------------------------------------------------------------
  178. %
  179. %    The vdm environment
  180. %
  181. \def\vdm{\@changeMathmodeCatcodes\@postUnderPenalty10000 }
  182.  
  183. % after an \end{vdm} the next paragraph is not indented unless a \par
  184. % comes first
  185. \def\endvdm{\global\let\par=\@undonoindent
  186.   \global\everypar={{\setbox0=\lastbox}\global\everypar={}%
  187.             \global\let\par=\@@par}}
  188.  
  189. \def\@undonoindent{\global\everypar={}\global\let\par=\@@par\@@par}
  190.  
  191. %-----------------------------------------------------------------
  192. %
  193. %     Controlling line and page breaks
  194. % 
  195. % Text within the vdm environment is essentially mathematical in
  196. % nature, so requires special care.  Whenever outer vertical mode is
  197. % entered, the \@beginVerticalVDM command should be used.  This sets
  198. % up \leftskip, \rightskip, \baselineskip, \lineskip and
  199. % \lineskiplimit to conform with the overall style.
  200. %
  201. % When entering unrestricted horizontal mode, the \@beginHorizontalVDM
  202. % command should be used.  This sets up:
  203. %    \leftskip and \rightskip to 0,
  204. %    \\ to do line breaking
  205. %    ragged right line breaking, with special penalties, and
  206. %    enters math mode.
  207. % \@endHorizontalVDM should be called when leaving unrestricted
  208. % horizontal mode.
  209.  
  210. \def\@beginVerticalVDM{\@changeMargins\@changeBaselineskip}
  211.  
  212. \def\@beginHorizontalVDM{\@restoreLineSeparator
  213.   \@restoreMargins\@raggedRight\noindent$\strut\relax}
  214. \def\@endHorizontalVDM{\relax\strut$}
  215.  
  216. % \VDMindent is used for \leftskip within VDM, \VDMrindent for
  217. % \rightskip, \VDMbaselineskip for \baselineskip
  218. \newdimen\VDMindent \VDMindent=\parindent
  219. \newdimen\VDMrindent \VDMrindent=\parindent
  220. \def\VDMbaselineskip{\baselineskip}
  221.  
  222. \def\@changeMargins{\leftskip=\VDMindent \rightskip=\VDMrindent}
  223. \def\@restoreMargins{\advance\hsize by-\leftskip
  224.   \advance\hsize by-\rightskip
  225.   \leftskip=0pt \rightskip=0pt}
  226. \def\@changeBaselineskip{\baselineskip=\VDMbaselineskip
  227.   \lineskip=0pt \lineskiplimit=0pt
  228.   % need to alter the size of struts, too
  229.   \setbox\strutbox\hbox{\vrule height.7\baselineskip
  230.       depth.3\baselineskip width\z@}}
  231.  
  232. % these are used in externals, records and cases
  233. \def\@changeLineSeparator{\let\\=\cr} % for usr within \halign
  234. \def\@restoreLineSeparator{\let\\=\newline}
  235.  
  236. \def\@raggedRight{\rightskip=0pt plus 1fil
  237.   \hyphenpenalty=-100 \linepenalty=200
  238.   \binoppenalty=10000 \relpenalty=10000 \pretolerance=-1}
  239.  
  240. %------------------------------------------------------------------------
  241. %
  242. %    Font and Character Changes
  243. %
  244. % make a-zA-Z use the \it family within math mode, and ~ mean \hook.
  245. % Digits 0-9 remain as normal.
  246. \newcount\@mathFamily  \@mathFamily=\itfam
  247. \everymath=\expandafter{\the\everymath\fam\@mathFamily
  248.     \@changeMathmodeCatcodes}
  249. \everydisplay=\expandafter{\the\everydisplay\fam\@mathFamily
  250.     \@changeMathmodeCatcodes}
  251. \mathcode`\0="0030
  252. \mathcode`\1="0031
  253. \mathcode`\2="0032
  254. \mathcode`\3="0033
  255. \mathcode`\4="0034
  256. \mathcode`\5="0035
  257. \mathcode`\6="0036
  258. \mathcode`\7="0037
  259. \mathcode`\8="0038
  260. \mathcode`\9="0039
  261.  
  262. % If the user really wants the normal codes, she can call \defaultMathcodes
  263. \def\defaultMathcodes{\@mathFamily=-1}
  264.  
  265. % make a : into punctuation, a - into a letter, and | mean \mid
  266. \ifps@
  267.  \def\@changeOtherMathcodes{\mathcode`\:="603A \mathcode`\-="002D
  268.   \mathcode`\|="327C \mathchardef\Or="32DA % this is a rel to get 5mu spacing
  269.   \mathcode`\f="0166} % normal letter spacing
  270. \else
  271.  \def\@changeOtherMathcodes{\mathcode`\:="603A \mathcode`\-="042D
  272.   \mathcode`\|="326A \mathchardef\Or="325F }% this is a rel to get 5mu spacing
  273. \fi
  274.  
  275. % alternative underscore
  276. \def\@VDMunderscore{\leavevmode
  277.   \kern.06em\vbox{\hrule\@height .2ex\@width .3em}\penalty\@postUnderPenalty
  278.   \hskip 0.1em}
  279.  
  280. % Allow line breaks after an underscore, but not in vdm mode (see
  281. % \vdm).  This is so long identifiers can be broken when run
  282. % into paragraphs. 
  283. \newcount\@postUnderPenalty \@postUnderPenalty=200
  284.  
  285. % now require some catcode trickery to enable us to change _ when we want to
  286. {\catcode`\_=\active \catcode`\"=\active
  287.  \gdef\@changeGlobalCatcodes{% make _ a normal char
  288.     \catcode`\_=\active \let_=\@VDMunderscore}
  289.  \gdef\@changeMathmodeCatcodes{%
  290.     % make ~ mean \hook, " do text, @ mean subscript
  291.     \let~=\hook
  292.     \catcode`\@=8
  293.     \catcode`\"=\active  \let"=\@mathText}
  294.  \gdef\underscoreoff{% make _ a normal char
  295.     \catcode`\_=\active \let_=\@VDMunderscore}
  296.  \gdef\underscoreon{% restore underscore to usual meaning
  297.     \catcode`\_=8}
  298.  \gdef\@mathText#1"{\hbox{\mathTextFont #1\/}}}
  299.  
  300. \def\mathTextFont{\rm}
  301.  
  302. %----------------------------------------------------------------
  303. %
  304. %    Keywords
  305. %
  306. \ifx\fmtname\@fmtname
  307.     \def\keywordFontBeginSequence{\small\sf}%    user-definable
  308. \else\ifx\fmtname\@psfmtname
  309.     \def\keywordFontBeginSequence{\sf}%    user-definable
  310. \else
  311.     \def\keywordFontBeginSequence{\bf}%    good for SliTeX
  312. \fi\fi
  313.  
  314. \def\kw#1{\hbox{\keywordFontBeginSequence #1\/}}
  315.  
  316. \def\makeNewKeyword#1#2{% use \newcommand for extra checks
  317.     \newcommand{#1}{\hbox{\keywordFontBeginSequence #2\/}}}
  318.  
  319. \makeNewKeyword{\nil}{nil}
  320. \makeNewKeyword{\True}{true}
  321. \makeNewKeyword{\true}{true}
  322. \makeNewKeyword{\False}{false}
  323. \makeNewKeyword{\false}{false}
  324.  
  325. \def\where{\par\moveright\VDMindent\hbox{\keywordFontBeginSequence where\/}}
  326.  
  327. %----------------------------------------------------------------
  328. %
  329. %    monadic operator creation
  330. %
  331. \def\newMonadicOperator#1#2{\newcommand{#1}{\kw{#2\kern.16667em}\nobreak}}
  332.  
  333. %----------------------------------------------------------------
  334. %
  335. %    primitive numeric types
  336. %
  337. % use the AMS fonts for these if possible
  338.  
  339. \ifams@
  340.   \mathchardef\Bool="0\msy@42    % Booleans
  341.   \mathchardef\Nat="0\msy@4E    % Natural numbers
  342.   \def\Nati{\Nat_1}        % Positive natural numbers
  343.   \mathchardef\Int="0\msy@5A    % Integers
  344.   \mathchardef\Real="0\msy@52    % Reals
  345.   \mathchardef\Rat="0\msy@51    % Rationals
  346. \else
  347.   \def\Bool{\hbox{\bf B\/}}
  348.   \def\Nat{\hbox{\bf N\/}}
  349.   \def\Nati{\hbox{$\hbox{\bf N}_1$}}
  350.   \def\Int{\hbox{\bf Z\/}}
  351.   \def\Real{\hbox{\bf R\/}}
  352.   \def\Rat{\hbox{\bf Q\/}}
  353. \fi
  354. \let\Natone=\Nati % just for an alternative
  355.  
  356. %----------------------------------------------------------------
  357. %
  358. %    Operations
  359. %
  360. % The op environment.  Within op you can specify args,
  361. % result, etc. which are gathered into registers, and output when the
  362. % op env. ends.
  363. %
  364. % The optional argument is the operation name
  365.  
  366. % shorthand for an operation on its own: the vdmop env.
  367. \def\vdmop{\vdm\op} \def\endvdmop{\endop\endvdm}
  368.  
  369. % registers constructed within an op environment
  370. \newtoks\@operationName
  371. \newbox\@operationNameBox
  372. \newif\ifArgumentListEncountered@
  373. \newtoks\@argumentListTokens
  374. \newtoks\@resultNameAndTypeTokens
  375. \newbox\@externalsBox
  376. \newbox\@preConditionBox
  377. \newbox\@postConditionBox
  378.  
  379. \def\op{% clear temporaries, deal with optional arg
  380.     \setbox\@operationNameBox=\hbox{}
  381.     \@argumentListTokens={} \ArgumentListEncountered@false
  382.     \@resultNameAndTypeTokens={}
  383.     \setbox\@externalsBox=\box\voidb@x
  384.     \setbox\@preConditionBox=\box\voidb@x
  385.     \setbox\@postConditionBox=\box\voidb@x
  386.     \par\preOperationHook
  387.     \vskip\preOperationSkip
  388.     \@beginVerticalVDM
  389.     \@ifnextchar [{\@opname}{}}
  390.  
  391. % breaking parameters
  392. \newcount\preOperationPenalty \preOperationPenalty=0
  393. \newcount\preExternalPenalty \preExternalPenalty=2000
  394. \newcount\prePreConditionPenalty \prePreConditionPenalty=800
  395. \newcount\prePostConditionPenalty \prePostConditionPenalty=500
  396. \newcount\postOperationPenalty \postOperationPenalty=-500
  397.  
  398. % gaps between bits of operations
  399. \newskip\preOperationSkip \preOperationSkip=2ex plus 0.5ex minus 0.2ex
  400. \newskip\postOperationSkip \postOperationSkip=2ex plus 0.5ex minus 0.2ex
  401. \newskip\postHeaderSkip \postHeaderSkip=.5ex plus .2ex minus .2ex
  402. \newskip\postExternalsSkip \postExternalsSkip=.5ex plus .2ex minus .2ex
  403. \newskip\postPreConditionSkip \postPreConditionSkip=.5ex plus .2ex minus .2ex
  404.  
  405. \def\endop{% make up operation
  406.     % IMPORTANT---don't remove the vskips in this macro
  407.     % if you don't want one, set it to 0pt
  408.     \vskip 0pt
  409.     \@setOperationHeader
  410.     \betweenHeaderAndExternalsHook
  411.     \vskip\postHeaderSkip
  412.     \ifvoid\@externalsBox
  413.           \betweenExternalsAndPreConditionHook
  414.     \else \moveright\VDMindent\box\@externalsBox
  415.           \betweenExternalsAndPreConditionHook
  416.           \vskip\postExternalsSkip
  417.     \fi
  418.     \ifvoid\@preConditionBox
  419.           \betweenPreAndPostConditionHook
  420.     \else \moveright\VDMindent\box\@preConditionBox
  421.           \betweenPreAndPostConditionHook
  422.           \vskip\postPreConditionSkip
  423.     \fi
  424.     \ifvoid\@postConditionBox
  425.           \postOperationHook
  426.     \else \moveright\VDMindent\box\@postConditionBox
  427.           \postOperationHook
  428.           \vskip\postOperationSkip
  429.     \fi}
  430.  
  431. % hooks for user-defined expansion
  432. % TeX is in outer vertical mode when these are called.
  433. % ALWAYS leave TeX in vertical mode after these macros have been called
  434. \def\preOperationHook{\penalty\preOperationPenalty }
  435. \def\betweenHeaderAndExternalsHook{\penalty\preExternalPenalty }
  436. \def\betweenExternalsAndPreConditionHook{\penalty\prePreConditionPenalty }
  437. \def\betweenPreAndPostConditionHook{\penalty\prePostConditionPenalty }
  438. \def\postOperationHook{\penalty\postOperationPenalty }
  439.  
  440. % combine the operation name, argument list and result
  441. \def\@setOperationHeader{%
  442.     \moveright\VDMindent\vtop{%
  443.         \ifArgumentListEncountered@
  444.             \setbox\@operationNameBox=
  445.                 \hbox{\unhbox\@operationNameBox\ $($}\fi
  446.         \hangindent=\wd\@operationNameBox \hangafter=1
  447.         \noindent\kern-.05em\box\@operationNameBox
  448.         \@beginHorizontalVDM
  449.         \ifArgumentListEncountered@\the\@argumentListTokens)\fi
  450.         \ \the\@resultNameAndTypeTokens
  451.         \@endHorizontalVDM}}
  452.  
  453. % set the operation name
  454. % \opname{name-of-operation}
  455. \def\opname#1{\@opname[#1]}
  456. \def\@opname[#1]{\@operationName={#1}%
  457.   \global\setbox\@operationNameBox=\hbox{$\relax#1$\ }}
  458.  
  459. % set up the argument list
  460. % \args{ argument \\ argument \\ argument... } where \\ forces a line break
  461. % This is also used in the fn environment
  462. \def\args{\global\ArgumentListEncountered@true \global\@argumentListTokens=}
  463.  
  464. % result name and type
  465. \def\res{\global\@resultNameAndTypeTokens=}
  466.  
  467. % externals list
  468. %
  469. % An external list could be either very long or very short, so we provide
  470. % two forms.  One is the short \ext{..} command, the other is the externals 
  471. % environment.
  472. % Externals are always separated by \\
  473. %
  474.  
  475. % we have to mess a little to get the catcode of : right
  476. \def\ext{\bgroup\@makeColonActive\@ext}
  477. \def\@ext#1{\externals#1\endexternals\egroup}
  478.  
  479. \def\externals{\global\setbox\@externalsBox=%
  480.     \@beginIndentedPara{\hsize}{ext }{\@setUpExternals}}
  481. \def\endexternals{\@endIndentedPara{\@endAlignment}}
  482.  
  483. \def\@setUpExternals{\@makeColonActive\@changeLineSeparator\@beginAlignment}
  484.  
  485. % more catcode trickery for :
  486. {\catcode`\:=\active
  487.  \gdef\@makeColonActive{\catcode`\:=\active \let:=&}}
  488.  
  489. % the \expandafters are necessary because TeX doesn't expand
  490. % \halign specs when scanning for # and &
  491. \def\@beginAlignment{\expandafter\halign\expandafter\bgroup
  492.     \the\@extAlign\strut\enspace&:\enspace$##$\hfil\cr}
  493. \def\@endAlignment{\crcr\egroup}
  494.  
  495. % the user can decide on the exact alignment of the field names
  496. \newtoks\@extAlign
  497. \def\leftExternals{\@extAlign={$##$\hfil}}
  498. \def\rightExternals{\@extAlign={\hfil$##$}}
  499. \leftExternals
  500.  
  501. \makeNewKeyword{\Rd}{rd } \makeNewKeyword{\Wr}{wr }
  502.  
  503. % pre-condition and post-condition
  504. %
  505. % once again we provide short forms \pre and \post, and environments
  506. % precond and postcond
  507. \def\pre#1{\precond#1\endprecond}
  508. \def\precond{\global\setbox\@preConditionBox=%
  509.     \@beginMathIndentedPara{\hsize}{pre }}
  510. \def\endprecond{\@endMathIndentedPara}
  511.  
  512. \def\post#1{\postcond#1\endpostcond}
  513. \def\postcond{\global\setbox\@postConditionBox=%
  514.     \@beginMathIndentedPara{\hsize}{post }}
  515. \def\endpostcond{\@endMathIndentedPara}
  516.  
  517.  
  518. %----------------------------------------------------------------
  519. %
  520. %    Box man\oe uvres
  521. %
  522. % Here's where all the tricky box manipulation commands go
  523. %
  524. % \@beginIndentedPara begins construction of a \hbox of width #1
  525. % which contains keyword #2 to the left of a para in a vtop.
  526. % #3 is evaluated within the inner vtop.
  527. % endIndentedPara closes the box off; its arg. is evaluated just
  528. % before closing the box.
  529. %
  530. \def\@beginIndentedPara#1#2#3{\hbox to #1\bgroup \setbox0=\kw{#2}%
  531.     \copy0 \strut \vtop\bgroup \advance\hsize by -\wd0 #3}
  532. \def\@endIndentedPara#1{\strut#1\egroup\hss\egroup}
  533.  
  534. % \@beginMathIndentedPara places the para in vdm mode
  535. \def\@beginMathIndentedPara#1#2{\@beginIndentedPara{#1}{#2}%
  536.     {\@beginHorizontalVDM}}
  537. \def\@endMathIndentedPara{\@endIndentedPara{\@endHorizontalVDM}}
  538.  
  539. % \@belowAndIndent#1#2 places #2 in a vbox below and to the right of #1
  540. \def\@belowAndIndent#1#2{#1\hfil\break
  541.     \@beginMathIndentedPara{\hsize}{\qquad}#2\@endMathIndentedPara}
  542.  
  543. %----------------------------------------------------------------
  544. %
  545. %    Constructions
  546. %
  547. % Here are all the standard constructions.
  548. % The only tricky one is \cases.
  549. % Those that construct a box must be made to make that box of 0 width,
  550. % and force a line break immediately afterwards.
  551.  
  552. % \If mm-exp \Then mm-exp \Else mm-exp \Fi
  553. % multi-line indented if-then-else
  554. %
  555. \def\If#1\Then#2\Else#3\Fi{\vtop{%
  556.     \@beginMathIndentedPara{0pt}{if }#1\@endMathIndentedPara
  557.     \@beginMathIndentedPara{0pt}{then }#2\@endMathIndentedPara
  558.     \@beginMathIndentedPara{0pt}{else }#3\@endMathIndentedPara}}
  559.  
  560. % \SIf mm-exp \Then mm-exp \Else mm-exp \Fi
  561. % single line if-then-else
  562. \def\SIf#1\Then#2\Else#3\Fi{\hbox to 0pt{\vtop{\@beginHorizontalVDM
  563.     \kw{if }\nobreak#1\penalty0\hskip 0.5em
  564.     \kw{then }\nobreak#2\penalty-100\hskip 0.5em % break here OK
  565.     \kw{else }\nobreak#3\@endHorizontalVDM}\hss}\hfil\break}
  566.  
  567. % \Let mm-exp \In mm-exp2
  568. % multi-line let..in ; mm-exp2 is `curried'
  569. \def\Let#1\In{\vtop{%
  570.     \@beginMathIndentedPara{0pt}{let }#1\hskip 0.5em
  571.     \kw{in}\@endMathIndentedPara}\hfil\break}
  572.  
  573. % \SLet mm-exp \In mm-exp
  574. % single-line let..in
  575. \def\SLet#1\In#2{\hbox to 0pt{\vtop{\@beginHorizontalVDM
  576.     \kw{let }\nobreak#1\hskip 0.5em
  577.     \kw{in }\penalty-200 #2\@endHorizontalVDM}\hss}\hfil\break}
  578.  
  579. % multi-line cases
  580. % 
  581. % \Cases{ selecting-mm-exp }
  582. % from-case1 & to-case1 \\
  583. % from-case2 & to-case2 \\
  584. %        ...
  585. % from-casen & to-casen
  586. % \Otherwise{ mm-exp }
  587. % \Endcases[optional text for the rest of the line]
  588.  
  589. \newif\ifOtherwiseEncountered@
  590. \newtoks\@OtherwiseTokens
  591.  
  592. \def\Cases#1{\hbox to 0pt\bgroup \vtop\bgroup
  593.         \@beginMathIndentedPara{\hsize}{cases }\strut
  594.             #1\hskip 0.5em\strut\kw{of}%
  595.         \@endMathIndentedPara
  596.         \bgroup % we might be in a nested case, so we have to
  597.             % save the \Otherwise bits we might lose
  598.         \OtherwiseEncountered@false \@changeLineSeparator 
  599.         \@beginCasesAlignment}
  600.  
  601. % the user can decide on the exact alignment
  602. \newtoks\@casesDef
  603. \def\leftCases{\@casesDef={$##$\hfil}}
  604. \def\rightCases{\@casesDef={\hfil$##$}}
  605. \rightCases
  606.  
  607. % the \expandafters are necessary because TeX doesn't expand
  608. % \halign specs when scanning for # and &
  609. \def\@beginCasesAlignment{\expandafter\halign\expandafter\bgroup
  610.     \the\@casesDef&$\,\rightarrow##$\hfil\cr}
  611.  
  612. \def\Otherwise{\global\OtherwiseEncountered@true \global\@OtherwiseTokens=}
  613.  
  614. \def\Endcases{\@endCasesAlignment \@setOtherwise \egroup \@setEndcases}
  615. \def\@endCasesAlignment{\crcr\egroup}
  616. \def\@setOtherwise{\ifOtherwiseEncountered@ % have an otherwise clause
  617.     \@beginMathIndentedPara{\hsize}{otherwise }%
  618.     \strut\the\@OtherwiseTokens\strut
  619.     \@endMathIndentedPara
  620.     \fi}
  621.  
  622. % must test for the optional arg to follow the end
  623. \def\@setEndcases{\noindent
  624.     \strut\kw{end}\@ifnextchar [{\@unbracket}{\@finalCaseEnd}}
  625. \def\@unbracket[#1]{$#1$\@finalCaseEnd}
  626. \def\@finalCaseEnd{\egroup\hss\egroup\hfil\break}
  627.  
  628. %----------------------------------------------------------------
  629. %
  630. %    special symbols
  631.  
  632. % defined as
  633. \ifps@
  634.  \def\DEF{\raise.5ex
  635.     \hbox{\footnotesize\underline{$\mathchar"3\cmsy@34$}}}% a \triangle
  636. \else
  637.  \def\DEF{\raise.5ex
  638.     \hbox{\footnotesize\underline{$\mathchar"3234$}}}% a \triangle
  639. \fi
  640.  
  641. % cross product
  642. \let\x=\times
  643.  
  644. %    logical connectives
  645. %
  646. \def\Iff{\penalty-50\mskip 7mu plus 2mu minus 2mu
  647.     \Leftrightarrow\mskip 7mu plus 2mu minus 2mu}
  648. \let\iff=\Iff
  649. \def\Implies{\penalty-35\mskip 6mu plus 2mu minus 1mu \Rightarrow
  650.     \mskip 6mu plus 2mu minus 1mu}
  651. \let\implies=\Implies
  652. % see changeOtherMathcodes for \Or
  653. \let\And=\land
  654. \let\and=\And
  655. %  use \neg for logical not, or
  656. \let\Not=\neg
  657.  
  658. %    quantification
  659. %
  660. \ifps@
  661.  \mathchardef\Exists="0224
  662.  \mathchardef\Forall="0222
  663.  \mathchardef\suchthat="22D7
  664. \else
  665.  \mathchardef\Exists="0239
  666.  \mathchardef\Forall="0238
  667.  \mathchardef\suchthat="2201
  668. \fi
  669. \def\exists{\@ifstar{\@splitExists}{\@normalExists}}
  670. \ifams@
  671.   \mathchardef\@nexists="0\msy@40 % crossed out existential quantifier
  672. \else
  673.   \def\@nexists{\hbox to 0pt{\raise0.15ex\hbox{/}\hss}\Exists}
  674. \fi
  675. \def\nexists{\@ifstar{\@splitNExists}{\@normalNExists}}
  676. \def\forall{\@ifstar{\@splitForall}{\@normalForall}}
  677. \def\unique{\@ifstar{\@splitUnique}{\@normalUnique}}
  678. \def\uniqueval{\@ifstar{\@splitUniqueval}{\@normalUniqueval}}
  679.  
  680. \def\@normalExists#1#2{{\Exists#1}\suchthat #2}
  681. \def\@normalNExists#1#2{{\@nexists#1}\suchthat #2}
  682. \def\@normalForall#1#2{{\Forall#1}\suchthat #2}
  683. \def\@normalUnique#1#2{{\Exists!\,#1}\suchthat #2}
  684. \def\@normalUniqueval#1#2{{\iota\,#1}\suchthat #2}
  685.  
  686. \def\@splitExists#1{\@belowAndIndent{\Exists#1\suchthat}}
  687. \def\@splitNExists#1{\@belowAndIndent{\@nexists#1\suchthat}}
  688. \def\@splitForall#1{\@belowAndIndent{\Forall#1\suchthat}}
  689. \def\@splitUnique#1{\@belowAndIndent{\Exists!\,#1\suchthat}}
  690. \def\@splitUniqueval#1{\@belowAndIndent{\iota\,#1\suchthat}}
  691.  
  692. %    strachey brackets
  693. %
  694. % (see TeXbook, p.437)
  695. \def\term#1{[\mkern-\thinmuskip[#1\relax]\mkern-\thinmuskip]}
  696.  
  697. %    function composition
  698. %
  699. \let\compf=\circ
  700.  
  701. %----------------------------------------------------------------
  702. %
  703. %    function environment
  704. %
  705. % This environment is similar to the op environment, but is used for
  706. % function definition.  
  707. %
  708. % The mandatory first parameter is the name of the function, the
  709. % second is the argument list.
  710. %
  711. % The *-form simply doesn't force the parentheses round the argument list
  712.  
  713. \def\fn{\parens@true\@beginVDMfunction}
  714. \@namedef{fn*}{\parens@false\@beginVDMfunction}
  715. \@namedef{endfn*}{\endfn}
  716.  
  717. % short form
  718. \def\vdmfn{\vdm\parens@true \@beginVDMfunction}
  719. \def\endvdmfn{\endfn\endvdm}
  720. \@namedef{vdmfn*}{\vdm\parens@false \@beginVDMfunction}
  721. \@namedef{endvdmfn*}{\endfn\endvdm}
  722.  
  723. % registers used within the fn environment
  724. \newtoks\@fnName
  725. \newbox\@fnNameBox
  726. \newif\ifsignatureEncountered@
  727. \newtoks\@signatureTokens
  728. \newbox\@fnDefnBox
  729. \newif\ifparens@
  730.  
  731. \def\@beginVDMfunction#1#2{%
  732.     \@fnName={#1}
  733.     \setbox\@fnNameBox=\hbox{$#1$}%
  734.     \setbox\@preConditionBox=\box\voidb@x % for people who want to do
  735.     \setbox\@postConditionBox=\box\voidb@x% implicit defns
  736.     \@signatureTokens={}\signatureEncountered@false
  737.     \ifparens@
  738.         \@argumentListTokens={(#2)}%
  739.     \else
  740.         \@argumentListTokens={#2}%
  741.     \fi
  742.     \par\preFunctionHook
  743.     \vskip\preFunctionSkip
  744.     \@beginVerticalVDM 
  745.     \@beginFnDefn}
  746.  
  747. % read in a signature
  748. \def\signature{\global\signatureEncountered@true \global\@signatureTokens=}
  749.  
  750. \def\@beginFnDefn{\global\setbox\@fnDefnBox=\vtop\bgroup
  751.     \hangindent=2em \hangafter=1 \@beginHorizontalVDM
  752.     \advance\hsize by-2em % this fools vboxes within the
  753.     % function body about the hanging indent...yuk.
  754.     % If you change the size of the indent, change the
  755.     % corresponding line in \endfn.
  756.     \copy\@fnNameBox \the\@argumentListTokens 
  757.     \quad\DEF\penalty-100\quad }
  758.  
  759. \newskip\preFunctionSkip \preFunctionSkip=2ex plus .5ex minus .2ex
  760. \newskip\postFunctionSkip \postFunctionSkip=2ex plus .5ex minus .2ex
  761. \newskip\betweenSignatureAndBodySkip
  762. \betweenSignatureAndBodySkip=1.2ex plus .3ex minus .2ex
  763. \newskip\betweenFunctionAndPreSkip
  764. \betweenFunctionAndPreSkip=1.2ex plus .3ex minus .2ex
  765.  
  766. \def\endfn{%
  767.     \advance\hsize by 2em% matches the dirty \advance in \@beginFnDefn
  768.     \@endHorizontalVDM
  769.     \egroup  % this ends the vtop we started in \@beginFnDefn
  770.     \ifsignatureEncountered@
  771.         \setbox0=\hbox{\unhbox\@fnNameBox$\;\mathpunct:\,$}%
  772.         \dimen255=\wd0 \noindent \box0
  773.         \vtop{\advance\hsize by-\dimen255 \@beginHorizontalVDM
  774.             \the\@signatureTokens \@endHorizontalVDM}\par
  775.         \betweenSignatureAndBodyHook
  776.         \vskip\betweenSignatureAndBodySkip
  777.     \fi
  778.     \moveright\VDMindent\box\@fnDefnBox
  779.     \ifvoid\@preConditionBox
  780.           \betweenPreAndPostConditionHook
  781.           \vskip\postFunctionSkip
  782.     \else \betweenFunctionAndPreHook
  783.           \vskip\betweenFunctionAndPreSkip
  784.           \moveright\VDMindent\box\@preConditionBox
  785.           \betweenPreAndPostConditionHook
  786.           \vskip\postPreConditionSkip
  787.     \fi
  788.     \ifvoid\@postConditionBox
  789.           \postFunctionHook
  790.     \else \moveright\VDMindent\box\@postConditionBox
  791.           \postFunctionHook
  792.           \vskip\postOperationSkip
  793.     \fi}
  794.  
  795. \newcount\preFunctionPenalty \preFunctionPenalty=0
  796. \newcount\betweenSignatureAndBodyPenalty \betweenSignatureAndBodyPenalty=500
  797. \newcount\betweenFunctionAndPrePenalty \betweenFunctionAndPrePenalty=1000
  798. \newcount\postFunctionPenalty \postFunctionPenalty=-500
  799.  
  800. % These are called in outer vertical mode---they must also exit in this mode
  801. \def\preFunctionHook{\penalty\preFunctionPenalty }
  802. \def\betweenSignatureAndBodyHook{\penalty\betweenSignatureAndBodyPenalty }
  803. \def\betweenFunctionAndPreHook{\penalty\betweenFunctionAndPrePenalty }
  804. \def\postFunctionHook{\penalty\postFunctionPenalty }
  805.  
  806. %    other function-related things
  807. %
  808.  
  809. % function arrow
  810. \def\to{\penalty-100\rightarrow}
  811.  
  812. % explicit lamdba function
  813. \def\LambdaFn{\@ifstar{\@splitLambdaFn}{\@normalLambdaFn}}
  814. \def\@normalLambdaFn#1#2{{\lambda#1}\suchthat#2}
  815. \def\@splitLambdaFn#1#2{% place body in a separate box below and to the right
  816.     {\lambda#1}\suchthat\hfil\break
  817.     \@beginMathIndentedPara{\hsize}{\qquad}#2\@endMathIndentedPara}
  818.  
  819. %----------------------------------------------------------------
  820. %
  821. %    Sets
  822.  
  823. % new set type
  824. \def\setof#1{\kw{set of }#1}
  825.  
  826. % set enumeration
  827. \def\set#1{\{#1\}}
  828.  
  829. % empty set
  830. \def\emptyset{\{\,\}}
  831.  
  832. % usual LaTeX operators apply: \in \notin \subset \subseteq
  833. \let\inter=\cap \let\intersection=\inter
  834. \let\Inter=\bigcap \let\Intersection=\Inter
  835. \let\union=\cup
  836. \let\Union=\bigcup
  837. \ifps@
  838.  \mathchardef\minus="222D
  839. \else
  840.  \mathchardef\minus="2200
  841. \fi
  842. \def\diff{\minus} \let\difference=\diff
  843.  
  844. \newMonadicOperator{\card}{card}
  845. \newMonadicOperator{\Min}{min}
  846. \newMonadicOperator{\Max}{max}
  847.  
  848. %----------------------------------------------------------------
  849. %
  850. %     Map type
  851.  
  852. % new map type
  853. \def\mapof#1#2{\kw{map }\nobreak#1\penalty-50\hskip .3em \kw{to }\nobreak#2}
  854.  
  855. % one-one map
  856. \def\mapinto#1#2{\kw{map }\nobreak#1\penalty-50
  857.     \hskip .3em \kw{into }\nobreak#2}
  858.  
  859. % map enumeration
  860. \def\map#1{\{#1\}}
  861.  
  862. % empty map
  863. \def\emptymap{\{\,\}}
  864.  
  865. %    map operators
  866. %
  867. % use \mapsto for |->
  868. % overwrite
  869. \def\owr{\dagger}
  870.  
  871. \ifams@
  872.   % domain restriction
  873.   \mathchardef\dres="2\msx@43
  874.   % range restriction
  875.   \mathchardef\rres="2\msx@42 % the right hand version
  876. \else % for those without AMS fonts
  877.   \let\dres=\lhd
  878.   \let\rres=\rhd
  879. \fi
  880.  
  881. % domain subtraction
  882. \ifps@
  883.  \def\dsub{\mathbin{\hbox{$\rlap{$\mathord\minus$}\mkern-1.5mu\dres$}}}
  884. \else
  885.  \def\dsub{\mathbin{\hbox{$\rlap{$\mathord\minus$}\mkern-1.5mu
  886.     \lower.1ex\hbox{$\dres$}$}}}
  887. \fi
  888.  
  889. % range subtraction
  890. \ifps@
  891.  \def\rsub{\mathbin{\hbox{$\rlap{$\mathord\minus$}\mkern-1.5mu\rres$}}}
  892. \else
  893.  \def\rsub{\mathbin{\hbox{$\rlap{$\mathord\minus$}\mkern-1.5mu
  894.     \lower.1ex\hbox{$\rres$}$}}}
  895. \fi
  896.  
  897. \newMonadicOperator{\dom}{dom}
  898. \newMonadicOperator{\rng}{rng}
  899.  
  900. %----------------------------------------------------------------
  901. %
  902. %    Sequences
  903. %
  904.  
  905. % new type
  906. \def\seqof#1{\kw{seq of }#1}
  907.  
  908. % enumeration
  909. \def\seq#1{[#1]}
  910.  
  911. % empty sequence
  912. \def\emptyseq{[\,]}
  913.  
  914. \newMonadicOperator{\len}{len}
  915. \newMonadicOperator{\hd}{hd}
  916. \newMonadicOperator{\tl}{tl}
  917. \newMonadicOperator{\elems}{elems}
  918. \newMonadicOperator{\inds}{inds}
  919. \def\cons#1{\kw{cons}\nobreak(#1)}
  920.  
  921. % sequence concatenation
  922. \ifams@
  923.   \mathchardef\sconc="2\msy@79
  924. \else
  925.   % this is truly yukky
  926.   \def\sconc{\mathbin{\hbox{\raise1ex\hbox{$\frown$}\kern-0.47em
  927.     \raise0.2ex\hbox{\it\char"12}}}}
  928. \fi
  929.  
  930. % distributed concatenation
  931. \newMonadicOperator{\Conc}{conc}
  932.  
  933. %----------------------------------------------------------------
  934. %
  935. %    type equation
  936. %
  937. \newtoks\@typeName
  938. \def\type#1#2{{\@typeName{#1} \preTypeHook \vskip\preTypeSkip
  939.     \@beginVerticalVDM
  940.     \moveright\VDMindent\vtop{\@beginHorizontalVDM #1=#2
  941.         \@endHorizontalVDM}
  942.     \postTypeHook \vskip\postTypeSkip}}
  943.  
  944. \def\preTypeHook{} \def\postTypeHook{}
  945. \newskip\preTypeSkip \preTypeSkip=1.2ex plus .5ex minus .3ex
  946. \newskip\postTypeSkip \postTypeSkip=1.2ex plus .5ex minus .3ex
  947.  
  948. %----------------------------------------------------------------
  949. %
  950. %    Composite Objects
  951. %
  952.  
  953. % literal composition; we have a compose and a composite env.
  954.  
  955. % single line compose
  956. \@namedef{composite*}#1{\kw{compose }$\relax#1\relax$\kw{ of }$\relax}
  957. \@namedef{endcomposite*}{\relax$\kw{ end}}
  958.  
  959. % multiple line version
  960. \def\composite#1{\bgroup\vskip\preCompositeSkip
  961.     \@beginVerticalVDM
  962.     \moveright\VDMindent\vtop\bgroup
  963.     \@beginHorizontalVDM
  964.     \kw{compose }#1\kw{ of}%\hfil\break
  965.     \@endHorizontalVDM
  966.     \@makeColonActive\@changeLineSeparator
  967.     \expandafter\halign\expandafter\bgroup\expandafter\qquad
  968.         \the\@recordAlign\strut\enspace&:\enspace$##$\hfil\cr}
  969. \def\endcomposite{\crcr\egroup % closes \halign
  970.     \kw{end}\egroup % ends the \vtop
  971.     \vskip\postCompositeSkip\egroup}
  972.  
  973. \def\scompose#1#2{\@nameuse{composite*}{#1}{#2}\@nameuse{endcomposite*}}
  974.  
  975. \newskip\preCompositeSkip \preCompositeSkip=1.2ex plus .5ex minus .3ex
  976. \newskip\postCompositeSkip \postCompositeSkip=1.2ex plus .5ex minus .3ex
  977.  
  978. % record composites; likewise we have a short and a long form
  979. \newtoks\@recordName
  980.  
  981. \def\record#1{\@recordName{#1}
  982.   \par\preRecordHook
  983.   \vskip\preRecordSkip
  984.   \@beginVerticalVDM
  985.   \moveright\VDMindent\hbox\bgroup
  986.       \setbox0=\hbox{$#1$\enspace::\enspace}%
  987.       \@makeColonActive\@changeLineSeparator
  988.       \advance\hsize by-\wd0 \box0
  989.       \@restoreMargins
  990.       %
  991.       % the \expandafters are necessary because TeX doesn't expand
  992.       % \halign specs when scanning for # and &
  993.       \vtop\bgroup\expandafter\halign\expandafter\bgroup
  994.           \the\@recordAlign\strut\enspace&:\enspace$##$\hfil\cr}
  995.  
  996. \def\endrecord{\crcr\egroup% closes halign
  997.     \egroup% closes vtop
  998.     \egroup% closes hbox
  999.     \par\postRecordHook
  1000.     \vskip\postRecordSkip}
  1001.  
  1002. % the user can decide on the exact alignment of the field names
  1003. \newtoks\@recordAlign
  1004. \def\leftRecord{\@recordAlign={$##$\hfil}}
  1005. \def\rightRecord{\@recordAlign={\hfil$##$}}
  1006. \rightRecord
  1007.  
  1008. % more catcode trickery
  1009. \def\defrecord{\bgroup\@makeColonActive\@defrecord}
  1010. \def\@defrecord#1#2{\record{#1}#2\endrecord\egroup}
  1011.  
  1012. \newskip\preRecordSkip \preRecordSkip=.75ex plus .3ex minus .2ex
  1013. \newskip\postRecordSkip \postRecordSkip=.75ex plus .3ex minus .2ex
  1014. \newcount\preRecordPenalty \preRecordPenalty=0
  1015. \newcount\postRecordPenalty \postRecordPenalty=-100
  1016. \def\preRecordHook{\penalty\preRecordPenalty }
  1017. \def\postRecordHook{\penalty\postRecordPenalty }
  1018.  
  1019. % \chg: mu function on composites
  1020. \def\chg#1#2#3{\mu(#1,#2\mapsto#3)}
  1021.  
  1022. %----------------------------------------------------------------
  1023. %
  1024. %    Hooks
  1025. %
  1026. % hooked identifiers --- these are taken from the TeXbook, p.357, 359
  1027. \ifps@
  1028.  \def\leftharpoonupfill{$\m@th \mathord\leftharpoonup \mkern-6mu
  1029.   \cleaders\hbox{$\mkern-2mu \mathchar"0\cmsy@00 \mkern-2mu$}\hfill
  1030.   \mkern-6mu \mathchar"0\cmsy@00$}  % p.357, \leftarrowfill
  1031. \else
  1032.  \def\leftharpoonupfill{$\m@th \mathord\leftharpoonup \mkern-6mu
  1033.   \cleaders\hbox{$\mkern-2mu \mathord\minus \mkern-2mu$}\hfill
  1034.   \mkern-6mu \mathord\minus$}  % p.357, \leftarrowfill
  1035. \fi
  1036. \def\overleftharpoonup#1{{%
  1037.   \boxmaxdepth=\maxdimen % this fixes Lamport's figures, but isn't necessary
  1038.                % for versions after 15 Dec 87
  1039.   \vbox{\ialign{##\crcr % p.359, \overleftarrow
  1040.     \leftharpoonupfill\crcr\noalign{\kern-\p@\nointerlineskip}
  1041.     $\hfil\displaystyle{#1}\hfil$\crcr}}}}
  1042.  
  1043. \let\hook=\overleftharpoonup  % c'est simple comme bonjour
  1044.  
  1045. %-----------------------------------------------------------------
  1046. %
  1047. %     General formula environment, a bit like \[ \] but is
  1048. %    indented to \VDMindent and will take \\
  1049. %
  1050. %
  1051. \def\form#1{\formula #1\endformula}
  1052.  
  1053. \def\formula{\par\preFormulaHook
  1054.     \vskip\preFormulaSkip
  1055.     \@beginVerticalVDM
  1056.     \bgroup
  1057.     \moveright\VDMindent\vtop\bgroup\@beginHorizontalVDM}
  1058. \def\endformula{\@endHorizontalVDM\egroup % ends the vtop
  1059.     \egroup % ends the overall group
  1060.     \par\postFormulaHook
  1061.     \vskip\postFormulaSkip}
  1062.  
  1063. \newskip\preFormulaSkip \preFormulaSkip=1.2ex plus .5ex minus .3ex
  1064. \newskip\postFormulaSkip \postFormulaSkip=1.2ex plus .5ex minus .3ex
  1065. \newcount\preFormulaPenalty \preFormulaPenalty=0
  1066. \newcount\postFormulaPenalty \postFormulaPenalty=-100
  1067. \def\preFormulaHook{\penalty\preFormulaPenalty }
  1068. \def\postFormulaHook{\penalty\postFormulaPenalty }
  1069.  
  1070. %----------------------------------------------------------------
  1071. %
  1072. %    Formula within a box, when width is unknown
  1073. %
  1074. %    equivalent to \parbox[t]{\hsize}{\@beginHorizontalVDM
  1075. %        ...\@endHorizontalVDM}
  1076. %
  1077. \def\formbox{\vtop\bgroup\@beginHorizontalVDM}
  1078. \def\endformbox{\strut\@endHorizontalVDM\egroup}
  1079.  
  1080. %----------------------------------------------------------------
  1081. %
  1082. %    special font for constants
  1083. %
  1084. \def\constantFont{\sc}
  1085. \def\const#1{\hbox{\constantFont #1\/}}
  1086.  
  1087. %----------------------------------------------------------------
  1088. %
  1089. %    line break and indent
  1090. %
  1091. \def\T#1{\\\hbox to #1em{}}
  1092.  
  1093. %----------------------------------------------------------------
  1094. %
  1095. %    line break and push line after to RHS
  1096. %
  1097. \def\R{\\\hspace*{\fill}}
  1098.  
  1099. %----------------------------------------------------------------
  1100. %
  1101. %    Proofs
  1102. %
  1103. % a proof environment for typesetting proofs in the "natural
  1104. % deduction" style.
  1105.  
  1106. \newdimen\ProofIndent \ProofIndent=\VDMindent
  1107. \newdimen\ProofNumberWidth \ProofNumberWidth=\parindent
  1108.  
  1109. \def\proof{\par\preProofHook
  1110.     \vskip\preProofSkip
  1111.     \let\&=\@proofLine
  1112.     \moveright\ProofIndent\vtop\bgroup
  1113.         \@indentLevel=1
  1114.         \advance\linewidth by-\ProofIndent
  1115.         \begin{tabbing}%
  1116.         \hbox to\ProofNumberWidth{}\=\kill}    % template line
  1117. \def\endproof{\end{tabbing}\advance\linewidth by\ProofIndent
  1118.     \egroup % ends the \vtop
  1119.     \par\postProofHook
  1120.     \vskip\postProofSkip}
  1121.  
  1122. \newskip\preProofSkip \preProofSkip=1.2ex plus .5ex minus .3ex
  1123. \newskip\postProofSkip \postProofSkip=1.2ex plus .5ex minus .3ex
  1124.  
  1125. \newcount\preProofPenalty \preProofPenalty=-100
  1126. \newcount\postProofPenalty \postProofPenalty=0
  1127. \def\preProofHook{\penalty\preProofPenalty }
  1128. \def\postProofHook{\penalty\postProofPenalty }
  1129.  
  1130. \def\From{\@indentProof\kw{from }\=%
  1131.     \global\advance\@indentLevel by 1
  1132.     \@enterMathMode}
  1133. \def\Infer{\global\advance\@indentLevel by-1
  1134.     \@indentProof\kw{infer }\@enterMathMode}
  1135. \def\@proofLine{\@indentProof\@enterMathMode}
  1136. \def\by{\`}
  1137.  
  1138. \newcount\@indentLevel
  1139. \newcount\@indentCount
  1140. \def\@indentProof{% do \>, \@indentLevel times
  1141.     \global\@indentCount=\@indentLevel
  1142.     \@gloop \>\global\advance\@indentCount by-1
  1143.     \ifnum\@indentCount>0
  1144.     \repeat}
  1145.  
  1146. % need special loop macros that works in across boxes
  1147. \def\@gloop#1\repeat{\gdef\@body{#1}\@giterate}
  1148. \def\@giterate{\@body \global\let\@gloopNext=\@giterate
  1149.     \else \global\let\@gloopNext=\relax \fi \@gloopNext}
  1150.  
  1151. % this enters math mode and sets the LaTeX macros \@stopfield up
  1152. % to exit math mode
  1153. \def\@enterMathMode{\def\@stopfield{$\egroup}$}
  1154.  
  1155. %----------------------------------------------------------------
  1156. \def\VDMauthor{M.Wolczko,
  1157. CS Dept.,
  1158. Univ. of Manchester, UK. 
  1159. mario@uk.ac.man.cs.ux
  1160. mcvax!man.cs.r5!mario}
  1161.  
  1162. \def\VDMversion{2.5}
  1163.  
  1164. \typeout{vdm style option <25 Mar 88>}
  1165. %----------------------------------------------------------------
  1166. %
  1167. %    Global changes
  1168. %
  1169. % All things that have to be invoked before the user's stuff appears
  1170. % should go here.
  1171. %
  1172. % by default the math spacing and changes to @ and _ apply everywhere
  1173. \@changeOtherMathcodes \@changeGlobalCatcodes
  1174. %
  1175. %-------------------the end--------------------------------------
  1176. \endinput
  1177. %
  1178. %    Summary of penalties
  1179. %
  1180. %    Penalties in vertical mode
  1181. %
  1182. % \preOperationPenalty        before an op begins
  1183. % \preExternalPenalty        between the header and externals of an op
  1184. % \prePreConditionPenalty    before the precondition
  1185. % \prePostConditionPenalty    before the postcondition
  1186. % \postOperationPenalty        at the end of an op
  1187. %
  1188. % \preFunctionPenalty        before a fn begins
  1189. % \betweenSignatureAndBodyPenalty 
  1190. % \postFunctionPenalty        after a fn ends
  1191. %
  1192. % \preRecordPenalty        before a record
  1193. % \postRecordPenalty        after a record
  1194. %
  1195. %    etc for formula, proof
  1196. %
  1197. %    Penalties in horizontal mode in boxes
  1198. %
  1199. % \linepenalty            101        \@raggedRight
  1200. % `if mm-exp ^ then..'        0        \SIf
  1201. % `if ... then mm-exp ^ else'    -100        \SIf
  1202. % `let mm-exp in ^ ...'        -200        \SLet
  1203. % `map mm-exp ^ to ...'        -50        \map
  1204. % ^\iff                -50        \iff
  1205. % ^\implies            -35        \implies
  1206. % func(args) \DEF^        -100        \begin{fn}
  1207. % \binoppenalty            10000
  1208. % \relpenalty            10000
  1209. % \hyphenpenalty        -100        \suchthat
  1210. % ^\to                -100        \to
  1211. % _^                100        \@VDMunderscore
  1212. %
  1213.